Nuprl Definition : es-interval 11,40

[ee'] == filter((ev.es-ble{i:l}(es;e;ev)); append(before(e'); cons(e'; []))) 
latex



clarification:

es-interval{i:l}
es-interval(esee')
== filter((ev.es-ble{i:l}(eseev)); append(es-before(ese'); cons(e'; []))) 
latex


Definitions[ee'], filter(Pl), es-ble{i:l}(es;e;e'), append(asbs), before(e)
FDL editor aliaseses-interval

origin